FDL - Step of Proof: p-fun-exp-add

Step of Proof: p-fun-exp-add

11,40

Inference at *
Iof proof for Lemma p-fun-exp-add:

T:Type, n, m:

, f:(T

(T + Top)). f^n+m = f^n o f^m

by (Auto

)

CollapseTHEN ((RWO "p-fun-exp-compose" 0)

CollapseTHEN ((Auto')

CollapseTHEN ((

CUnfold `p-fun-exp` ( 0)

)

CollapseTHEN ((GenConcl p-id() = id THENA Auto)

CollapseTHEN (

CRWO "primrec_add" 0 THEN Auto THEN Reduce 0 THEN Auto)

)

Definitions s = t, x:AB(x), left + right, Top, p-id(), Type, f^n, P Q, P & Q, x:A B(x), P Q, #$n, primrec(n;b;c), x.A(x), f o g , t T, {i..j}, x:A. B(x), , {x:A| B(x)} , , A B, A, False, P Q

Lemmas p-fun-exp-compose, p-id wf, primrec add, primrec wf, p-compose wf, int seg wf

Definitions	s = t, x:AB(x), left + right, Top, p-id(), Type, f^n, P Q, P & Q, x:A B(x), P Q, #$n, primrec(n;b;c), x.A(x), f o g , t T, {i..j}, x:A. B(x), , {x:A\| B(x)} , , A B, A, False, P Q
Lemmas	p-fun-exp-compose, p-id wf, primrec add, primrec wf, p-compose wf, int seg wf